Nuprl Lemma : w-when-lemma
0,22
postcript
pdf
T
:Type,
w
:World.
FairFifo
(
e
:E,
x
:Id. vartype(loc(
e
);
x
)
T
state_when(
e
).
x
= (
x
when
e
)
T
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
s(
i
;
t
).
x
,
f
(
a
)
,
P
Q
,
False
,
A
,
A
B
,
,
{
x
:
A
|
B
(
x
) }
,
,
x
:
A
B
(
x
)
,
vartype(
i
;
x
)
,
s
=
t
,
Prop
,
b
,
x
:
A
B
(
x
)
,
E
,
time(
e
)
,
loc(
e
)
,
(
x
when
e
)
,
s
.
x
,
state_when(
e
)
,
Type
,
World
,
FairFifo
,
Id
,
<
a
,
b
>
Lemmas
w-vartype
wf
,
w-loc
wf
,
Id
wf
,
w-E
wf
,
fair-fifo
wf
,
world
wf
,
w-state-when
,
w-s
wf
origin
T:Type, w:World.
(e:E, x:Id. vartype(loc(e);x) 
T state_when(e).x = (x when e) 
T) T:Type, w:World.
(e:E, x:Id. vartype(loc(e);x) T state_when(e).x = (x when e) T) Tx:A. B(x) Q
A
B
B(x)
b
B(x)